es:ES, T:Type, I:MaInterface(T), i:Id.
(i  ma-interface-locs(I))
 ma-interface-consistent2(es;I)
 (e:E.
 ((e  [[I|i]]))  (can-apply(ma-interface-code(I;i;kind(e))((state when e));val(e)))) 

latex

Definitions

P  Q, x:A. B(x), False, A, left + right, P  Q, Dec(P), ES, t  T, Type, MaInterface(T), Id, ma-interface-locs(I), ma-interface-consistent2(es;I), E, ma-interface-consistent(es;X), [[I|i]], e  X, b, Knd, ma-interface-dom(I;i), kind(e), (x  l), can-apply(f;x), es-triggers(es;i;ds;conds), IdDeq, f(x), t.2, KindDeq, x  dom(f), , x:A  B(x), a:A fp B(a), Atom$n, s = t, a < b, e@i. P(e), t.1, if b then t else f fi , x. t(x), {x:A| B(x)} , State(ds), Top, x:AB(x), type List, fpf-domain(f), P  Q, P & Q, P  Q, Void, x:A.B(x), x:A. B(x), let x,y = A in B(x;y), case b of inl(x) => s(x) | inr(y) => t(y), <a, b>, hasloc(k;i), S  T, , x.A(x), IdLnk, True, b, a = b, p q, p  q, T, {T}, SQType(T), s ~ t, ma-interface-info(I;i;k), ma-interface-code(I;i;k)

Lemmas

id-deq wf, fpf wf, Knd wf, IdLnk wf, Kind-deq wf, es-kind wf, bool cases, eqtt to assert, assert of band, and functionality wrt iff, bool sq, eqff to assert, squash wf, true wf, bnot thru band, assert of bor, or functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, band wf, bool wf, bor wf, eq id wf, bnot wf, not wf, subtype rel product, subtype rel list, subtype rel function, decl-state wf, top wf, subtype rel set, hasloc wf, subtype-set-hasloc, member-fpf-domain, l member subtype, fpf-ap wf, fpf-dom wf, pi2 wf, fpf-trivial-subtype-top, assert wf, es-is-interface wf, ma-interface-triggers wf, es-E wf, ma-interface-consistent2 wf, l member wf, ma-interface-locs wf, Id wf, ma-interface wf, event system wf, ma-interface-triggers-loc, decidable l member, decidable equal Kind, ma-interface-triggers-kind, ma-interface-consistent-consistent2